Hey! It looks like you've submitted a new PR for the library teams!

If this PR contains changes to any rust-lang/rust public library APIs then please comment with @rustbot label +T-libs-api -T-libs to tag it appropriately. If this PR contains changes to any unstable APIs please edit the PR description to add a link to the relevant API Change Proposal or create one if you haven't already. If you're unsure where your change falls no worries, just leave it as is and the reviewer will take a look and make a decision to forward on if necessary.

Examples of T-libs-api changes:

• Stabilizing library features
• Introducing insta-stable changes such as new implementations of existing stable traits on existing stable types
• Introducing new or changing existing unstable library APIs (excluding permanently unstable features / features without a tracking issue)
• Changing public documentation in ways that create new stability guarantees
• Changing observable runtime behavior of library APIs

r? @joshtriplett

(rust-highfive has picked a reviewer for you, use r? to override)

@rustbot author

I made a small fix in a7a048f1ed1e91d6dad6b69396e16a5d41d8e240 to use the wording "distinct" instead of "different" (which is the correct mathematical term, I believe).

I didn't incorporate the other edits yet, see my comments/questions on the review.

@rustbot label -S-waiting-on-author +S-waiting-on-review

I think the distinction drawn between "weak ordering" and "total ordering" is wishy-washy outside of its mathematical context, and it's counterproductive to appeal to language like "distinct (mathematical) objects".

What is a distinct mathematical object? Are two Strings with the same contents, but different capacities, "distinct"? What about two Strings that contain the same text and capacity but at different memory locations? What about two i32s? There's no generic "mathematical" sense of equality that applies; it depends on the type and on the semantic value imputed to the idea of "comparison".

I take the position that String::from("foo") and String::from("foo") are the same element of the set of values represented by the type String. They have different representations in the physical computer because they are placed at different memory locations, but they represent the same abstract idea of "a string containing foo". So it makes sense to me that String::from("foo") == String::from("foo") is true.

Similarly, in the poker example you could argue that two poker hands with the same value are the same hand, with different representations - the exact representation chosen not mattering for the purpose of the program being written, in the same way that the exact location of foo in memory doesn't matter for the vast majority of programs that use String. The fact that we have equality of references defined in terms of the underlying objects, IMO, supports this interpretation.

From this perspective, trying to distinguish between a weak order and a total order on the grounds of reflexivity makes no sense. The relation is what defines the distinct-ness of members of the set; to argue that one 14 and another 14 are "distinct mathematical objects" (which nevertheless happen to be equal) is missing the point of viewing sets as types entirely. I think the only really hard rule we have to recognize is reflexivity of an object with its identity, e.g. a == a when a is actually a local or static variable, not an expression. (make_foo() == make_foo() has no such constraint, regardless of how trivial make_foo is, because for some types identity is the interesting quality that we use to define distinctness.)

What is a distinct mathematical object?

An object that isn't the same as another object.

The difficulty is that

• two values being the same (as in mathematical equality) and
• the == operator

are not the same.

However, Ord is (currently) claimed to be a total order because == is (wrongly) assumed to reflect mathematical equality, which isn't always true (or at least depends on semantics). In particular, a == b does not imply that a and b are non-distinguishable.

Are two Strings with the same contents, but different capacities, "distinct"?

That depends on definition/semantics.

What about two i32s?

If their value is equal, they are the same (indistinguishable).

We can implement a type where two values a and b show different properties even though a == b evaluates to true. Neither the rules of PartialEq nor the rules of Eq forbid this. In that case, claiming that Ord is a total order is a mistake or at least depends on semantics, because the condition "a = b" in the antisymmetric property (If a ≤ b and b ≤ a then a = b) (see Wikipedia) must match the == operator in Rust (for which there is no requirement).

See also @steffahn's comment here.

From this perspective, trying to distinguish between a weak order and a total order on the grounds of reflexivity makes no sense.

Note that the PR does not distinguish between a weak order and a total order based on reflexivity. Reflexivity (which is required by Eq) demands that a == a for every a. The distinction is made on whether a == b can be true for two mathematically non-equal objects / values (which is neither required by PartialEq nor by Eq).

What is a distinct mathematical object?

An object that isn't the same as another object.
This is a meaningless definition though. What does it mean for two objects to be "the same"?

I hereby define "sameness", mathematically, as "returning true when compared with ==".

The difficulty is that

* two values being the _same_ (as in mathematical equality) and
* the `==` operator

are not the same.

I declare that they are the same. Therefore, there is no difficulty.

However, Ord is (currently) claimed to be a total order because == is (wrongly) assumed to reflect mathematical equality

In my interpretation, Ord is a total order, because == is the definition of mathematical equality.

which isn't true (or at least depends on semantics). In particular, a == b does not imply that a and b are non-distinguishable.

"distinguishable" is a curious term; let's come back to this.

Are two Strings with the same contents, but different capacities, "distinct"?

That depends on definition/semantics.

Precisely. They are distinct for some purposes but not others. Which puts your notion of "distinct (mathematical) object" on shaky ground.

What about two i32s?

If their value is equal, they are the same (indistinguishable).

They are not indistinguishable: I can distinguish between two i32s with different addresses. I could write an equivalence relation (not PartialEq, obviously, because of coherence) that does distinguish between those i32s based on address and not value. Would you then say that every i32 is a distinct mathematical object? That means that the notion of "distinct mathematical object" is not independent of the implementation of PartialEq. So as far as I'm concerned, I am happy to continue allowing == to define "distinct mathematical object", insofar as that term has any value over Rust code.

We can implement a type where two values a and b show different properties even though a == b evaluates to true.

As I mentioned above, i32 is an example of such a type, and the property that is different is its address.

The problem with this extreme position is that it isn't useful to think of all i32s with the same content but different addresses as distinct elements of a set; it is useful to have a concept of sameness beyond reference equality, and that concept is PartialEq.

I think where you are going wrong is in thinking "types are sets, and objects are members". I would argue that types represent sets, and objects represent members. It is fine to have multiple objects that represent the same member of the set, in a mathematically abstract sense. I could argue, mathematically, all poker hands with the same value but different cards represent the same member of the set Hand, in the same way that all i32s with the same bit pattern represent the same member of the set of all possible 32-bit signed integers. (Of course, it would be silly to write a poker game this way but that is not the point. People write silly things sometimes; the discussion here is about what "sameness" and "distinct" mean.)

I hereby define "sameness", mathematically, as "returning true when compared with ==".

I declare that [two values being the same (as in mathematical equality) and the == operator] are the same. Therefore, there is no difficulty.

You can make these definitions/declarations, but for the sake of a factual discussion, do you know of any notion in the Rust documentation that == is the same as mathematical equality (i.e. indistinguishability)?

The Rust reference defines the == as "equal", which would backup your interpretation at first sight. But == is also provided by PartialEq. If == is always mathematical equality, then we wouldn't need an Eq trait, because mathematical equality implies reflexivity, thus Eq would have to be implemented always (which it isn't).

In short: == cannot be the same as mathematical equality because mathematical equality is reflexive and == sometimes isn't.

Moreover, I would claim that -0.0 == 0.0 is another counter-evidence for your hypothesis because -0.0 and 0.0 are not equal in regard to calculation rules (they yield different results when being used in a computation).

Moreover, I don't see any requirement in the docs which demand that == must be implemented according to "equality" in the mathematical sense. Using the term "equality" in the context of programming can have a different meaning than in the context of mathematics. Yet "total order" is a mathematical term that should be used correctly when adopted by Rust's documentation.

I think you could be right if Eq implies more than reflexivity (in addition to the requirements of PartialEq). But I don't think that is the case, and I don't think it's planned/intended to add such a requirement to Eq.

You can make these definitions/declarations, but for the sake of a factual discussion, do you know of any notion in the Rust documentation that == is the same as mathematical equality (i.e. indistinguishability)?

Mathematical equality of the represented objects is not the same as indistinguishability of their Rust representations.

For example, two different Vecs may represent the same mathematical object (the sequence [3, 1, 4, 1, 5]), and yet they may be distinguishable in their API: their capacities are different, and the public capacity() method returns different values.

I think it is correct to say that Eq represents equality.

Now PartialEq is weird, because mathematically there is no such thing as "partial equality". And if it's supposed to stand for "the partial equivalence relation" then it's also weird, because there is more than one partial equivalence relation on integers, and there is no such thing as "the default one". If you say "the (partial or not) equivalence relation on integers" to a mathematician, they will ask you: "Which one?". It makes no sense for a trait to say it is "the (partial) equivalence relation" without specifying what you're talking about in more detail. It has to mention "equality".

I consider PartialEq a crazy special version of "equality" that solely exists to support the crazy IEEE-754's concept of f64 and f32 "equality".

Mathematical equality of the represented objects is not the same as indistinguishability of their Rust representations.

For example, two different Vecs may represent the same mathematical object (the sequence [3, 1, 4, 1, 5]), and yet they may be distinguishable in their API: their capacities are different, and the public capacity() method returns different values.

I would say it isn't clear (or well-defined) whether "mathematical equality" is the same as "indistingushability" in the context of programming. It's a question of semantics, but an important one because it ultimately influences whether Ord describes a total order or a weak order.

If and only if == (semantically) denotes mathematical equality, then Ord denotes a total order. (This is what the PR aims to clarify.) But == isn't the same as mathematical equality in the general case (because it's provided by PartialEq and not required to be reflexive).

But let's look (again) at == under the condition that Eq is implemented (which is the case when Ord is implemented as Eq is a supertrait of Ord):

I think it is correct to say that Eq represents equality.

If that was true, then Eq and PartialEq would differ in more aspects than just demanding reflexivity. In particular: Implementing Eq would imply certain semantics (in addition to demanding reflexivity). And I don't think that's the case (or is that somewhere documented?). Adding this demand would be ("semantically" viewed) a breaking change because existing implementations of Eq in certain crates would need to be removed if they use Eq for equivalence relations that are not semantically identical to mathematical equality.

Hence I don't think Eq represents equality in the mathematical sense. Instead, I would take the stance that it is an equivalence relation.

Now PartialEq is weird, because mathematically there is no such thing as "partial equality". And if it's supposed to stand for "partial equivalence relation" then it's also weird, because there is more than one partial equivalence relation on integers.

The term "partial equality" has been removed by this PR.

It is not a problem that there are different partial equivalence relations. Implementing PartialEq means that one of those relations is implemented. (There are also different total (pre)orders, of which only one can be implemented.)

I think it is correct to say that Eq represents equality.

If that was true, then Eq and PartialEq would differ in more aspects than just demanding reflexivity. In particular: Implementing Eq would imply certain semantics (in addition to demanding reflexivity). And I don't think that's the case (or is that somewhere documented?).

The semantics of Eq, meaning "equality", are documented in the first sentence of the docs: "Trait for equality comparisons".

The later demand that it be an equivalence relation (on representations) exists because user types don't specify their intended mathematical interpretation in code. Any equivalence relation defines a mathematical interpretation. Any equivalence relation R on a set (of representations) creates another set (the quotient set of equivalence classes) of "mathematical interpretations" such that R(x, y) <=> Interpretation(x) = Interpretation(y).

The semantics of Eq, meaning "equality", are documented in the first sentence of the docs: "Trait for equality comparisons".

I thought so at first too, but the same phrase is used in PartialEq here. Thus I conclude that here "equality comparison" refers to the equality operator and not to mathematical equality.

Note that this PR removes that phrase (both in Eq and PartialEq) to avoid ambiguity.

Hence I don't think Eq represents equality in the mathematical sense. Instead, I would take the stance that it is an equivalence relation.

My problem with this is that it doesn't say which equivalence relation. There is no default one for integers! It sounds like it just implements an arbitrary one for i32 and you can't assume which one. Not only is it less intuitive, it's less precise mathematically.

For orders it's a bit different because when you say "the total order on integers" people generally know what you're talking about because there is a default order on integers. If you say "the equivalence relation on integers" to me, rather than "equality", I would be puzzled because I don't know which equivalence relation you're talking about, and if you meant "equality" you would just say that.

My problem with this is that it doesn't say which equivalence relation. There is no default one for integers! It sounds like it just implements an arbitrary one for i32 and you can't assume which one. Not only is it less intuitive, it's less precise mathematically.

I understand your concerns, but adding such a demand (for the general case) would go beyond the scope of this PR (and arguably be a breaking change). Moreover, I don't think it's necessary to restrict Eq to a particular equivalence relation.

Regarding i32 or other concrete types in std, there could be a note added how PartialEq or PartialOrd are implemented for those types. But I also see this as out of scope for this PR.

For orders it's a bit different because when you say "the total order on integers" people generally know what you're talking about because there is a default order on integers. If you say "the equivalence relation on integers" to me, rather than "equality", I would be puzzled because I don't know which equivalence relation you're talking about, and if you meant "equality" you would just say that.

That is pretty subjective. The situation for Eq and Ord is the same: There exist multiple equivalence relations of which only one can be implemented through Eq and there exist multiple total (pre)orders of which only one can be implemented through Ord.

Moreover, I don't think it's necessary to restrict Eq to a particular equivalence relation.

I agree. I didn't suggest there is. This doesn't contradict the idea that Eq is equality.

For instance, in poker, you can implement Eq on hands to take the order of cards into account, in which case your type represents ordered sequences of cards. Or you can implement it such that it treats different orders as equal, in which case it semantically represents sets of cards. In each case it is still "equality" on whatever your type semantically represents.

This doesn't contradict the idea that Eq is equality.

Do you mean mathematical equality or the equality comparison using the equality operator? This ambiguity is one of the things that this PR aims to solve.

For instance, in poker, you can implement Eq on hands to take the order of cards into account, in which case your type represents ordered sequences of cards. Or you can implement it such that it treats different orders as equal, in which case it semantically represents sets of cards. In each case it is still "equality" on whatever your type semantically represents.

According to my understanding, there is only one form of equality in mathematics (opposed to equivalence relations, of which there can exist many). The only way to

• allow different implementations of Eq while also
• demanding that Eq is mathematical equality

would be to require the user/programmer to define mathematical equality in a particular way (if Eq is used). This would be somewhat awkward and the wrong way: I don't think the Rust documentation can or should tell people how to define mathematical equality. It should be the other way around. Moreover, it means that the mathematical definition changes when the implementation of PartialEq::eq changes. This isn't a well usable model, in my opinion, and would be twisted.

Do you mean mathematical equality

Yes, for types that represent mathematical objects.

The only way to allow different implementations of Eq while also demanding that Eq is mathematical equality would be to require the user/programmer to define mathematical equality in a particular way (if Eq is used). I don't think the Rust documentation can or should tell people how to define mathematical equality.

Nobody "defines mathematical equality". In mathematics, everybody knows already what equality means, nobody redefines equality.

I already gave an example with poker hands where Eq can conceivably be defined in one of two different ways, and both of these ways are compatible with the standard mathematical concept of equality. What changes isn't "how mathematics defines equality", what changes is what kind of mathematical objects the type represents.

It should be the other way around.

It is the other way round. You first think about what mathematical objects your type represents, and then you implement Eq accordingly to match that semantics.

You first think about what mathematical objects your type represents, and then you implement Eq accordingly to match that semantics.

I agree that you can proceed like that. But this means that if you implement Eq, and if PartialEq::(a, b) is true for some objects a and b, then these objects must be indistinguishable in the mathematical model the programmer uses. I.e. your proposal is to forbid implementations of Eq in certain cases, depending on the mathematical model the programmer has in mind.

Of course that's possible, but I doubt it's useful. An advantage would be that Ord is clearly a total order in that case (because you restrict the programmer).

The problem with demanding "mathematical equality" in order to be allowed to implement Eq (beside being arguably a breaking change) is that equality (in the mathematical sense) is a huge restriction: It makes objects indistinguishable in the mathematical model.

Given that == is implemented by PartialEq (and not by Eq), it's already clear that the == operator is used in a broader sense than only to indicate mathematical equality.

@tczajka I would like to add that this PR doesn't forbid the programmer to use mathematical models and the Eq trait according to your ideas. It only explains the consequences of the programmer's choice.

The new section in Ord, which this PR proposes:

Weak orders

Depending on how PartialEq::eq is implemented for a type, two different values a and b may result in a == b, even though they describe two distinct (mathematical) objects. If that can be the case, then Ord actually describes a weak order (or total preorder) instead of a total order.

Ord only describes a total order if a == b corresponds to equality in the mathematical sense (i.e. if it is is not true for two distinct values a and b).

This is just a consequence of the current status-quo, which I don't aim to change.

Considering alternatives to this PR (in regard to Eq and Ord), I could see the following ways to go:

1. Leave documentation as is

This would mean that terms like "total equality" and "partial equality" are used, which aren't well-defined. Moreover, the use of the phrase "equality comparison" is ambiguous. That phrase is used for Eq as well as PartialEq, thus cannot mean mathematical equality (because PartialEq doesn't fulfill reflexivity). Moreover, either

• Ord being a total order, or
• Eq only demanding reflexivity in addition to the constraints of PartialEq

is wrong.

I therefore see a need to update the docs in that matter.

2. Clarify that Ord isn't always a total order (which is what this PR does)

This seems to describe the current status-quo in the best way and it doesn't restrict the programmer (or their model) in unnecessary ways.

3. Add additional constraints to Eq

It could be demanded that Eq must only be implemented when PartialEq::eq indicates mathematical equality (and not any other equivalence relation). This could arguably be seen as a breaking change, even though it only affects semantics:

As explained in my previous post, it requires the mathematical model to ensure indistinguishability between two mathematical objects a and b if PartialEq::eq(a, b) is true and Eq is implemented. Thus this restriction would be (in regard to the models used) very huge. It is also a bit odd in cases where there is no (strict) mathematical model used by the programmer.

The only advantage would be that Ord is then formally a total order (because the programmer is forced to not implement Eq otherwise).

I corrected the typo in "mathematically" (12ed8a8) and replaced "this" with "this trait" (b71d6bc).

On my side, I'm ready to go.

@bors r=@workingjubilee

📌 Commit b71d6bc has been approved by workingjubilee

It is now in the queue for this repository.

Ooops, I hope replacing "this" with "this trait" was alright for you. (It seemed to be approved instantly after I did the "bors r=you" thing.

Yeah, that's fine.

Please squash the fixup commits.

@bors r-

Please squash the fixup commits.

@RalfJung I squashed them (86b031b). Anything else I need to do?

No, seems good to go, thanks. :)
@bors r=workingjubilee

📌 Commit 86b031b has been approved by workingjubilee

It is now in the queue for this repository.

@bors rollup

⌛ Testing commit 86b031b with merge 3bcad65...

☀️ Test successful - checks-actions
Approved by: workingjubilee
Pushing 3bcad65 to master...

Finished benchmarking commit (3bcad65): comparison URL.

Overall result: ✅ improvements - no action needed

@rustbot label: -perf-regression

Instruction count

This is a highly reliable metric that was used to determine the overall result at the top of this comment.

Max RSS (memory usage)

Cycles

This benchmark run did not return any relevant results for this metric.

Binary size

This benchmark run did not return any relevant results for this metric.

Bootstrap: 623.65s -> 621.776s (-0.30%)
Artifact size: 271.98 MiB -> 271.95 MiB (-0.01%)